SherbyNet - /page/wikibook/entry.mu

Micron Document

<!DOCTYPE html>

<title>Java Modeling Language</title>

</head>

Java Modeling Language

</h1>

</header>

/* start https://en.wikipedia.org/ */

.mw-parser-output .ambox{border:1px solid #a2a9b1;border-left:10px solid #36c;background-color:#fbfbfb;box-sizing:border-box}.mw-parser-output .ambox+link+.ambox,.mw-parser-output .ambox+link+style+.ambox,.mw-parser-output .ambox+link+link+.ambox,.mw-parser-output .ambox+.mw-empty-elt+link+.ambox,.mw-parser-output .ambox+.mw-empty-elt+link+style+.ambox,.mw-parser-output .ambox+.mw-empty-elt+link+link+.ambox{margin-top:-1px}html body.mediawiki .mw-parser-output .ambox.mbox-small-left{margin:4px 1em 4px 0;overflow:hidden;width:238px;border-collapse:collapse;font-size:88%;line-height:1.25em}.mw-parser-output .ambox-speedy{border-left:10px solid #b32424;background-color:#fee7e6}.mw-parser-output .ambox-delete{border-left:10px solid #b32424}.mw-parser-output .ambox-content{border-left:10px solid #f28500}.mw-parser-output .ambox-style{border-left:10px solid #fc3}.mw-parser-output .ambox-move{border-left:10px solid #9932cc}.mw-parser-output .ambox-protection{border-left:10px solid #a2a9b1}.mw-parser-output .ambox .mbox-text{border:none;padding:0.25em 0.5em;width:100%}.mw-parser-output .ambox .mbox-image{border:none;padding:2px 0 2px 0.5em;text-align:center}.mw-parser-output .ambox .mbox-imageright{border:none;padding:2px 0.5em 2px 0;text-align:center}.mw-parser-output .ambox .mbox-empty-cell{border:none;padding:0;width:1px}.mw-parser-output .ambox .mbox-image-div{width:52px}@media(min-width:720px){.mw-parser-output .ambox{margin:0 10%}}@media print{body.ns-0 .mw-parser-output .ambox{display:none!important}}

/* end https://en.wikipedia.org/ */

</style>

The Java Modeling Language (JML) is a <a href="Specification_language" title="Specification language">specification language</a> for <a href="Java_(programming_language)" title="Java (programming language)">Java</a> programs, using <a href="Hoare_logic" title="Hoare logic">Hoare style</a> <a href="Precondition" title="Precondition">pre-</a> and <a href="Postcondition" title="Postcondition">postconditions</a> and <a href="Invariant_(computer_science)" class="mw-redirect" title="Invariant (computer science)">invariants</a>, that follows the <a href="Design_by_contract" title="Design by contract">design by contract</a> paradigm. Specifications are written as <a href="Java_annotation" title="Java annotation">Java annotation</a> comments to the source files, which hence can be compiled with any Java <a href="Compiler" title="Compiler">compiler</a>.

Various verification tools, such as a runtime assertion checker and the Extended Static Checker (<a href="ESC/Java" title="ESC/Java">ESC/Java</a>) aid development.

<div class="mw-heading mw-heading2"><h2 id="Overview">Overview</h2></div>

JML is a behavioural interface specification language for Java modules. JML provides <a href="Semantics" title="Semantics">semantics</a> to formally describe the behavior of a Java module, preventing ambiguity with regard to the module designers' intentions. JML inherits ideas from <a href="Eiffel_(programming_language)" title="Eiffel (programming language)">Eiffel</a>, <a href="Larch_family" title="Larch family">Larch</a> and the <a href="Refinement_Calculus" class="mw-redirect" title="Refinement Calculus">Refinement Calculus</a>, with the goal of providing rigorous formal semantics while still being accessible to any Java programmer. Various tools are available that make use of JML's behavioral specifications. Because specifications can be written as annotations in Java program files, or stored in separate specification files, Java modules with JML specifications can be compiled unchanged with any Java compiler.

<div class="mw-heading mw-heading2"><h2 id="Syntax">Syntax</h2></div>

JML specifications are added to Java code in the form of annotations in comments. Java comments are interpreted as JML annotations when they begin with an @ sign. That is, comments of the form

</pre></div>

or

<div class="mw-highlight mw-highlight-lang-java mw-content-ltr" dir="ltr"><pre> /*@ <JML specification> @*/

</pre></div>

Basic JML syntax provides the following keywords

<dl><dt><code>requires</code></dt>

<dd>Defines a <a href="Precondition" title="Precondition">precondition</a> on the <a href="Method_(computer_science)" class="mw-redirect" title="Method (computer science)">method</a> that follows.</dd>

<dt><code>ensures</code></dt>

<dd>Defines a <a href="Postcondition" title="Postcondition">postcondition</a> on the method that follows.</dd>

<dt><code>signals</code></dt>

<dd>Defines a postcondition for when a given <a href="Exception_handling" title="Exception handling">Exception</a> is thrown by the method that follows.</dd>

<dt><code>signals_only</code></dt>

<dd>Defines what exceptions may be thrown when the given precondition holds.</dd>

<dt><code>assignable</code></dt>

<dd>Defines which fields are allowed to be assigned to by the method that follows.</dd>

<dd>Declares a method to be side effect free (like <code>assignable \nothing</code> but can also throw exceptions). Furthermore, a pure method is supposed to always either terminate normally or throw an exception.</dd>

<dt><code>invariant</code></dt>

<dd>Defines an <a href="Class_invariant" title="Class invariant">invariant property of the class</a>.</dd>

<dt><code>loop_invariant</code></dt>

<dd>Defines a <a href="Loop_invariant" title="Loop invariant">loop invariant</a> for a loop.</dd>

<dd>Combines specification cases and can also declare that a method is inheriting specifications from its supertypes.</dd>

<dt><code>assert</code></dt>

<dd>Defines a JML <a href="Assertion_(computing)" class="mw-redirect" title="Assertion (computing)">assertion</a>.</dd>

<dt><code>spec_public</code></dt>

<dd>Declares a protected or private variable public for specification purposes.</dd></dl>

Basic JML also provides the following expressions

<dl><dt><code>\result</code></dt>

<dd>An identifier for the return value of the method that follows.</dd>

<dd>A modifier to refer to the value of the <code><expression></code> at the time of entry into a method.</dd>

<dt><code>(\forall <decl>; <range-exp>; <body-exp>)</code></dt>

<dd>The <a href="Universal_quantifier" class="mw-redirect" title="Universal quantifier">universal quantifier</a>.</dd>

<dt><code>(\exists <decl>; <range-exp>; <body-exp>)</code></dt>

<dd>The <a href="Existential_quantifier" class="mw-redirect" title="Existential quantifier">existential quantifier</a>.</dd>

<dd><code>a</code> implies <code>b</code></dd>

<dd><code>a</code> is implied by <code>b</code></dd>

as well as standard <a href="Java_syntax" title="Java syntax">Java syntax</a> for logical and, or, and not. JML annotations also have access to Java objects, object methods and operators that are within the scope of the method being annotated and that have appropriate visibility. These are combined to provide formal specifications of the properties of classes, fields and methods. For example, an annotated example of a simple banking class may look like

<div class="mw-highlight mw-highlight-lang-java mw-content-ltr" dir="ltr"><pre>public class BankingExample

{

public static final int MAX_BALANCE = 1000;

private /*@ spec_public @*/ boolean isLocked = false;

//@ public invariant balance >= 0 && balance <= MAX_BALANCE;

//@ assignable balance;

//@ ensures balance == 0;

public BankingExample()

{

this.balance = 0;

}

//@ requires 0 < amount && amount + balance < MAX_BALANCE;

//@ assignable balance;

//@ ensures balance == \old(balance) + amount;

public void credit(final int amount)

{

this.balance += amount;

}

//@ requires 0 < amount && amount <= balance;

//@ assignable balance;

//@ ensures balance == \old(balance) - amount;

public void debit(final int amount)

{

this.balance -= amount;

}

//@ ensures isLocked == true;

public void lockAccount()

{

this.isLocked = true;

}

//@ requires !isLocked;

//@ ensures \result == balance;

//@ also

//@ requires isLocked;

//@ signals_only BankingException;

public /*@ pure @*/ int getBalance() throws BankingException

{

if (!this.isLocked)

{

return this.balance;

}

else

{

throw new BankingException();

}

}

</pre></div>

Full documentation of JML syntax is available <a rel="nofollow" class="external text" href="http://jmlspecs.org/jmlrefman/jmlrefman_toc.html">in the JML Reference Manual</a>.

<div class="mw-heading mw-heading2"><h2 id="Tool_support">Tool support</h2></div>

A variety of tools provide functionality based on JML annotations. The Iowa State JML tools provide an assertion checking <a href="Compiler" title="Compiler">compiler</a> <code>jmlc</code> which converts JML annotations into runtime assertions, a documentation generator <code>jmldoc</code> which produces <a href="Javadoc" title="Javadoc">Javadoc</a> documentation augmented with extra information from JML annotations, and a unit test generator <code>jmlunit</code> which generates <a href="JUnit" title="JUnit">JUnit</a> test code from JML annotations.

Independent groups are working on tools that make use of JML annotations. These include:

<ul><li><a href="ESC/Java2" class="mw-redirect" title="ESC/Java2">ESC/Java2</a> <a rel="nofollow" class="external autonumber" href="https://web.archive.org/web/20051016013145/http://secure.ucd.ie/products/opensource/ESCJava2/">[1]</a>, an extended static checker which uses JML annotations to perform more rigorous static checking than is otherwise possible.</li>

<li><a rel="nofollow" class="external text" href="http://www.openjml.org/">OpenJML</a> declares itself the successor of ESC/Java2.</li>

<li><a rel="nofollow" class="external text" href="http://pag.csail.mit.edu/daikon/">Daikon</a>, a dynamic invariant generator.</li>

<li><a href="KeY" title="KeY">KeY</a>, which provides an open source theorem prover with a JML front-end and an <a href="Eclipse_(software)" title="Eclipse (software)">Eclipse</a> plug-in (<a rel="nofollow" class="external text" href="http://www.key-project.org/eclipse/JMLEditing/">JML Editing</a>) with support for <a href="Syntax_highlighting" title="Syntax highlighting">syntax highlighting</a> of JML.</li>

<li><a rel="nofollow" class="external text" href="http://krakatoa.lri.fr">Krakatoa</a>, a static verification tool based on the <a rel="nofollow" class="external text" href="http://why.lri.fr">Why</a> verification platform and using the <a href="Coq_(software)" class="mw-redirect" title="Coq (software)">Coq</a> proof assistant.</li>

<li><a rel="nofollow" class="external text" href="http://jmleclipse.projects.cis.ksu.edu/">JMLEclipse</a>, a plugin for the Eclipse integrated development environment with support for JML syntax and interfaces to various tools that make use of JML annotations.</li>

<li><a rel="nofollow" class="external text" href="http://www.sireum.org/?q=node/21/">Sireum/Kiasan</a>, a symbolic execution based static analyzer which supports JML as a contract language.</li>

<li><a rel="nofollow" class="external text" href="http://www.eecs.ucf.edu/~leavens/JML2/docs/man/jmlunit.html">JMLUnit</a>, a tool to generate files for running JUnit tests on JML annotated Java files.</li>

<li><a rel="nofollow" class="external text" href="https://web.archive.org/web/20110706084805/http://www.dc.uba.ar/inv/grupos/rfm_folder/TACO">TACO</a>, an open source program analysis tool that statically checks the compliance of a Java program against its Java Modeling Language specification.</li></ul>

<div class="mw-heading mw-heading2"><h2 id="References">References</h2></div>

<ul><li><a href="Gary_T._Leavens" title="Gary T. Leavens">Gary T. Leavens</a> and Yoonsik Cheon. Design by Contract with JML; Draft tutorial.</li>

<li><a href="Gary_T._Leavens" title="Gary T. Leavens">Gary T. Leavens</a>, Albert L. Baker, and Clyde Ruby. JML: A Notation for Detailed Design; in Haim Kilov, <a href="Bernhard_Rumpe" title="Bernhard Rumpe">Bernhard Rumpe</a>, and Ian Simmonds (editors), Behavioral Specifications of Businesses and Systems, Kluwer, 1999, chapter 12, pages 175-188.</li>

<li><a href="Gary_T._Leavens" title="Gary T. Leavens">Gary T. Leavens</a>, Erik Poll, Curtis Clifton, Yoonsik Cheon, Clyde Ruby, David Cok, Peter Müller, Joseph Kiniry, Patrice Chalin, and Daniel M. Zimmerman. JML Reference Manual (DRAFT), September 2009. <a rel="nofollow" class="external text" href="http://www.jmlspecs.org/jmlrefman/jmlrefman_toc.html">HTML</a></li>

<li><a href="Marieke_Huisman" title="Marieke Huisman">Marieke Huisman</a>, Wolfgang Ahrendt, Daniel Bruns, and Martin Hentschel. Formal specification with JML. 2014. <a rel="nofollow" class="external text" href="http://primo.bibliothek.kit.edu/primo_library/libweb/action/dlDisplay.do?vid=KIT&docId=KITSRCE1000041881&tab=kit_evastar&srt=date">download (CC-BY-NC-ND)</a></li></ul>

<div class="mw-heading mw-heading2"><h2 id="External_links">External links</h2></div>

<ul><li><a rel="nofollow" class="external text" href="http://www.eecs.ucf.edu/~leavens/JML/index.shtml">JML website</a></li></ul></div><div><div class="zim-footer">

This article is issued from <a class="external text" title="Last edited on 2024-04-04" href="https://en.wikipedia.org/wiki/?title=Java_Modeling_Language&oldid=1217242146">Wikipedia</a>. The text is available under <a class="external text" href="https://creativecommons.org/licenses/by-sa/4.0/deed.en">Creative Commons Attribution-Share Alike 4.0</a> unless otherwise noted. Additional terms may apply for the media files.

</div>

</div></div>

</div>

</main>

</div>

</body></html>